COMMENT ⊗   VALID 00015 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.if false then begin "revision outline"
C00006 00003	.s(FOLISP,PROVING LISP PROGRAMS CORRECT)
C00011 00004	.ss Introductory Example.
C00018 00005	.ss First Order Logic with Conditional Forms and Lambda-expressions.
C00036 00006	.ss Conditional Expressions.
C00041 00007	.ss Lambda-expressions.
C00044 00008	.ss First Order Axioms for LISP.
C00050 00009	.ss Axiom Schemas of Induction.
C00054 00010	.ss A Simple Example. 
C00062 00011	.ss Pseudo-logic.
C00072 00012	.ss An Extended Example.
C00093 00013	.ss Functionals and Least Fixedpoints. 
C00106 00014	.ss The Minimization Schema.
C00114 00015	.cb Exercises.
C00121 ENDMK
C⊗;
.if false then begin "revision outline"
intro: motivation, automatic proving and checking, why develop f-o-theory

informal example: properties of append by list induction (theory.new)
	compare to numinduction?

informal discussion of what it means to formalize such an argument
	mention notions of language, semantics (intended model), 
	formal notion of proof, theory, 
	notion of fn defined by rec defn, 
	exists unique least defined partial fn on domain that satisfies fnl eqn
	"totality", "bottom" 

formalization:
   language
   semantics
   rules for manipulating sentences
	mentions some standard dedn rules
	rules for cond
	rules for λ
   axioms for theory of LISP (include cvi (istail and issexp) from the beginning
	mention not all independent, but are useful for making more natural proofs

really recursive functions
   definitions that are "total" on form 
   add to axioms fnl eqn and fact that ⊗islist() or ⊗issexp() or ⊗isnatnum
   mention reasonable list of forms and do formal example :length(fringe(x))=size(x)
   proving that a rec defn is really recursive  eg that result is in desired domain
   another example :flatten=fringe?

recursively defined predicates
    lose(x)←lose(x)
    representing fn
    arriving at desired equiv when rf is "total" (eg has only T and NIL as values)
    occur example
    istail upto commontail relations?

substantial example
    samefringe
    correctness of partions of a list into n pieces.  
	 show each part is a part 
	 show every part occurs
    balancing algorithm

how to handle definitions of partial fns
   motivation, example of kinds of interesting problems
   min schema 
   example of use

add selection of exercises to prove facts about the programs written as
    solutions to the exercises in Ch 2.

fix unification problem to be programming and proving problem

.end "revision outline"
.s(FOLISP,PROVING LISP PROGRAMS CORRECT)
.if NOTASSEMBLING then start
.IMPURE: NEXT SECTION!;
.SEARCH: NEXT SECTION!;
.EXTEND: NEXT SECTION!;
.ABSNTX: NEXT SECTION!;
.COMPIL: NEXT SECTION!;
.COMPUT: NEXT SECTION!;
.FOL←"A"
.end

	The theory of computation may be divided into
two parts.  The first is the general
theory of computability including topics like universal functions,
the existence of uncomputable functions, lambda calculus, call-by-name and
call-by-value, and the relation of conditional expression recursion
to other formalisms for describing computable functions.  The
second part, which we will discuss in this chapter emphasizes
techniques for proving particular facts about particular computable
functions.  We emphasize the use of the techniques
more than their mathematical background.  Much of the material in
this chapter is based on [Cartwright 1977] and the rest on [McCarthy 1977].

	We begin with proving ⊗extensional ⊗properties 
of ⊗clean, ⊗pure LISP programs.  An ⊗extensional ⊗property is one that
depends only on the function computed by the program.  Thus it
includes the fact that two sort programs compute the same function
or that ⊗append is associative but does not include the fact
that one sort program does ⊗⊗n%52%*⊗ comparisons and another ⊗⊗n_log_n⊗
comparisons.  ⊗Clean LISP programs have no side effects (our
methods require the freedom to replace a subexpression by an equal
expression), and equality refers to the S-expressions and not to
the list structures.  ⊗Pure LISP involves only recursive function
definitions and doesn't use assignment statements.
It wouldn't be difficult to give corresponding methods that would
be valid for non-functional programs, because this topic is well
developed.

	In spite of all these limitations, the techniques are useful and
point the way to further progress.
The main idea is to represent the programs formally using first order logic.
Higher order functionals and predicates are used informally.
Formal proofs of properties of programs can easily be checked using an 
automatic proof checker such as FOL [Weyhrauch 1977].    Examples are given in
Appendix {SECTION FOL}.

	We begin with an informal sample proof, commenting about the information
and concepts needed to make the proof work.  We then proceed to formalize these
ideas.  The  necessary basic facts can be divided into several categories:
first order logic including conditional forms and first order
lambda-expressions, algebraic facts about lists and S-expressions,
facts about the inductive structure of lists and
S-expressions, and general facts about functions defined by
recursion.
.ss Introductory Example.

	Consider the function ⊗append ( * ) defined by

⊗⊗⊗u * v ← if qn u qthen v qelse qa u . [qd u * v]⊗

and the predicate ⊗member ( ε ) defined by

⊗⊗⊗x ε u ← ¬qn u ∧ [x = qa u ∨ x ε qd u]	⊗

where ⊗x is any S-expression and ⊗u and ⊗v are lists (whose elements are 
S-expresssions).   (Note that our precedence conventions imply that  
⊗⊗qd u_*_v_=_[qd u]_*_v⊗.)   
It is probably intuitively clear that if ⊗x is a member of
one of the lists ⊗u or ⊗v then ⊗x is a member of the list ⊗⊗u_*_v⊗.   We will
give an informal proof of this property.

	The proof will be based on the principle of ⊗list_induction which is
analogous to natural induction (for functions on the natural numbers).
This principle states that if some property, qP(qNIL), holds for the list qNIL and
if, by assuming qP(⊗⊗u⊗) holds for ⊗⊗qd u⊗, we can prove that it holds for the list ⊗u 
then qP(⊗⊗u⊗) holds for all lists ⊗u.   In our case qP(⊗⊗u⊗) is the property:

⊗⊗⊗[x ε u ∨ x ε v] ⊃ x ε [u * v] .		⊗

The induction will be with respect to the list ⊗u, eg. the first argument to 
⊗append.  The variables ⊗x and ⊗v are just carried along. 

	The proof consists of two parts.  First we assume qn ⊗u.  Then by the
definition of ⊗member, ⊗⊗x_ε_u⊗ is false and by the definition of ⊗append, 
⊗⊗u_*_v_=_v⊗.  Thus qP(⊗⊗u⊗) becomes 

⊗⊗⊗x ε v ⊃ x ε v	⊗

which is true.

	Next we assume ¬qn ⊗u and that ⊗⊗qP(qd u)⊗ is true.  Thus 

⊗⊗⊗[x ε qd u ∨ x ε v] ⊃ x ε [qd u * v]⊗

By definition of ⊗append, ⊗⊗u_*_v⊗ reduces to ⊗⊗qa u . [qd u * v]⊗.  Thus
⊗⊗u_*_v_≠_qNIL⊗, ⊗⊗qa [u_*_v]_=_qa u⊗ and ⊗⊗qd [u_*_v]_=_qd u_*_v⊗.
By definition of ⊗member, ⊗⊗x_ε_u⊗ reduces to ⊗⊗x_=_qa u_∨_x_ε_qd u⊗.  So we
consider two cases: ⊗⊗x_=_qa u⊗  and  ⊗⊗x_ε_qd u_∨_x_ε_v⊗.  

	In the first case we have ⊗⊗x_=_qa [u_*_v]⊗ and so, by definition of
⊗member, ⊗⊗x_ε_[u_*_v]⊗ and qP(⊗⊗u⊗) is true.  In the second case we have
by the induction hypothesis that ⊗⊗x_ε_[qd u_*_v]⊗ and again, by definition of
⊗member,  qP(⊗⊗u⊗) holds.  

	Thus we have done the required proofs and by list induction the
property qP(⊗⊗u⊗) holds for any list ⊗u.  

.if lines < 7 then next page
	In carrying out the proof we have used properties of lists such as
.NOFILL

				⊗⊗[x . u]⊗ is a list
				⊗⊗qa [x . u] = x]⊗
				⊗⊗qd [x . u] = u]⊗
				⊗⊗¬qn [x . u]⊗
.FILL
for any S-expression ⊗x and any list ⊗u.  We have also used these properties
with ⊗u replaced by ⊗⊗u_*_v⊗ or ⊗⊗qd u_*_v⊗.  To do this we need to know that
⊗⊗u_*_v⊗ is a list or that ⊗⊗qd u_*_v⊗ is a list.  This is essentially the
same as saying that the computation defined by ⊗append terminates in a finite
number of steps or that ⊗append is a total function.  

	Saying that ⊗⊗u * v⊗ reduces to ⊗⊗qa u . [qd u * v]⊗ is based on the
rule for computing recursively defined functions.   It too, is only meaningful
when ⊗⊗qd u_*_v⊗ is a list, eg. when ⊗append is total.   
Note that in using the recursive function definition and the rule for comptation
we are essentially substituting equals for equals in the problem.  The two
cases can be combined giving the ⊗functional_equation for ⊗append  

⊗⊗⊗u * v = qif qn u qthen v qelse qa u . [qd u * v].⊗

Again, being  able to use the functional equation here 
depends on knowing ⊗append is total.

	Similiarly several of
the statements made about ⊗member depend on the fact that it is total.  Thus
to complete the proof it is necessary to know that ⊗append and ⊗member are
total.  This should be intuitively clear, since the recursive calls in the
definitions  depend on the ⊗cdr of the test variable and, since our lists
are finite, this will eventually be qNIL and the computation will terminate.
We will see later how to state and prove such facts.

	The validity of the list induction principle is due to the fact that
we require our lists to be finite.  
This just is one of many forms of induction.  We will see examples
of other forms as well as other applications of list induction.
Looking at induction in another way, 
if one starts with a set of properties that must be satisfied by a domain
and some basic functions on that domain,  then requiring that some induction
principle be valid  is a way of giving further information
about the domain.
.ss First Order Logic with Conditional Forms and Lambda-expressions.

	The logic we shall use is a sorted first order logic with equality,
extended by admitting conditional forms as terms and first
order lambda-expressions as function symbols.  These extensions do not
change the logical strength of the theory, because, as we shall see, every
formula that includes conditional forms or first order lambdas can be
transformed into an equivalent formula without them.  However, the
extensions are practically important, because they permit us to use
recursive definitions directly as formulas of the logic.  The adjective sorted
refers to the fact that we may restrict a variable to range 
over some type of object (a sort) rather than over all objects. We can then restrict
the domain of a function to some fixed sort.  This means that in
proving properties of that function attention can be focused on the domain 
of interest without worrying about what happens for arguments for which the
function is not intended to be defined.
For example, we shall often use the variables ⊗u and ⊗v to denote lists,
and the sorting will permit us to write statements that are true for
lists but not for general S-expressions without putting the fact that
their validity is restricted to lists into the statement itself.

	The language for our logic contains terms, formulas,
function expressions and predicate expressions which are
built from constants, variables,
predicate symbols, and function symbols using function application,
conditional terms, boolean terms, lambda expressions, and quantifiers.

%3Constants%1: We will use S-expresssions as constants standing for
themselves and also lower case letters from the first part
of the alphabet to represent constants in other domains than
S-expressions.  In particular we will have the atom qNIL.  Other atoms
will be introduced as needed.  Among the non-S-expression  constants 
we will have qw (read "bottom").

%3Variables%1: We will use the letters ⊗XX through ⊗ZZ 
as general variables.  The variables ⊗u through ⊗w  
will range over lists, while ⊗x through ⊗z will range over
S-expressions and ⊗X through ⊗Z range over extended S-expressions 
(the set consisting of S-expressions togther with the constant qw).
  ⊗k through ⊗n are integer variables.  Variables
ranging over other sorts will be introduced later, when it is meaningful.
The variables may appear with or without subscripts.


%3Function symbols%1:  As function constant symbols we will use
the LISP function names qqa, qqd and . (as an infix).
Other function symbols including function parameter symbols 
will be introduced as needed.
We suppose that each function symbol takes the same definite number of
arguments every time it is used.
Thus if the same letter is used with differing numbers of arguments,
it stands for different function symbols.
Thus we can use ⊗⊗<x%41%*, ... ,x%4n%*>⊗ to represent the list forming
functions, but we shall have to axiomatize it separately for each
length we actually use.
We will often use one argument functions symbols as prefixes, i.e.
without brackets, just as qqa and qqd have been used up to now.

%3Predicate symbols%1: 
As predicate constant symbols we will use the logical equality symbol =, and
the LISP predicate names qqat, qqn and qeq.  
We will use qP as a predicate parameter symbol. 
Certain unary predicate symbols will be designated as sorts. In particular
⊗isesexp, ⊗issexp and ⊗islist are sorts.  
Other predicate symbols and sorts will be introduced when needed.
We suppose that each predicate symbol takes the same definite
number of arguments each time it is used.
Again a letter may be used with differing numbers of arguments to
represent different predicates.
Infix and prefix notation will also be used where this is
customary.

	Next we define terms, formulas, function expressions
and predicate expressions inductively.  A term is
an expression whose value will be an object like an S-expression
or a number while a formula has value qtrue or qfalse.  We will use the
symbols T and F for the formulas always having the values qtrue and qfalse
respectively.
Terms are used in making formulas, and formulas occur in
terms so that the definitions are ⊗mutually ⊗recursive where
this use of the word ⊗recursive should be distinguished from
its use in recursive definitions of functions.
Function and predicate expressions are also involved in the mutual recursion.


%3Terms%1: Constants are terms, and variables are terms.  If
⊗f is a function expression taking ⊗n arguments, and ⊗⊗t%41%*,_..._,t%4n%*⊗
are terms, then ⊗⊗f[t%41%*,_..._,t%4n%*]⊗ is a term.  If ⊗s is
a formula and ⊗⊗t%41%*⊗ and ⊗⊗t%42%*⊗ are terms, then
⊗⊗qif_s_qthen_t%41%*_qelse_t%42%*⊗ is a term.  We soften the
notation by allowing infix symbols where this is customary.

%3Formulas%1:
T and F are formulas.
If ⊗⊗t%41%*⊗ and ⊗⊗t%42%*⊗ are terms then ⊗⊗t%41%*_=_t%42%*⊗ is a formula.
If qp is a predicate expression taking ⊗n arguments and
⊗⊗t%41%*,_..._,t%4n%*⊗ are terms, then ⊗⊗qp[t%41%*,_..._,t%4n%*]⊗ is
a formula.  
If ⊗s is a formula, then ¬⊗s is also a formula.  If
⊗⊗s%41%*⊗ and ⊗⊗s%42%*⊗ are formulas, then ⊗⊗s%41%*⊗_∧_⊗⊗s%42%*⊗, 
⊗⊗s%41%*⊗_∨_⊗⊗s%42%*⊗, ⊗⊗s%41%*⊗_⊃_⊗⊗s%42%*⊗, and
⊗⊗s%41%*⊗_≡_⊗⊗s%42%*⊗ are formulas.  If ⊗⊗s%40%*⊗, ⊗⊗s%41%*⊗ and ⊗⊗s%42%*⊗ are
formulas, then ⊗⊗qif_s%40%*_qthen_s%41%*_qelse_s%42%*⊗ is a formula.
If ⊗⊗x%41%*,_...,_x%4n%*⊗ are variables, and ⊗s is a formula, then
⊗⊗[∃x%41%*_..._x%4n%*:_s]⊗ and ⊗⊗[∀x%41%*_..._x%4n%*:_s]⊗ are formulas.

%3Function expressions%1: A function symbol is a function expression.
If ⊗⊗x%41%*,_..._,x%4n%*⊗ are variables and ⊗t is a term, then
⊗⊗[λx%41%*,_..._,x%4n%*:_t]⊗ is a function expression.

%3Predicate expressions%1: A predicate symbol is a predicate expression.
If ⊗⊗x%41%*,_..._,x%4n%*⊗ are variables and ⊗s is a formula, then
⊗⊗[λx%41%*,_..._,x%4n%*:_s]⊗ is a predicate expression.

	An occurrence of a variable ⊗x is called ⊗bound if
it is in an expression of one of the forms ⊗⊗[λx%41%*_..._x%4n%*:_t]⊗,
⊗⊗[λx%41%*_..._x%4n%*:_s]⊗, ⊗⊗[∀x%41%*_..._x%4n%*:_s]⊗ or ⊗⊗[∃x%41%*_..._x%4n%*:_s]⊗
where ⊗x is one
of the numbered ⊗⊗x⊗'s.  If not bound an occurrence is called ⊗free.  
A formula having no free variables is called a ⊗sentence.  

	The ⊗semantics of first order logic consists of the rules
that determine whether a formula is qtrue
or qfalse.  However, the truth or falsity of a formula is relative
to the interpretation assigned to the constants, the function and predicate
symbols and the free variables of the formula.  We proceed as follows:

	We begin by choosing a domain.  In most cases,
the domain will include the S-expressions, and any S-expression constants
appearing in the formula stand for themselves.  We will allow for the
possibility that other objects than S-expressions exist, and some constants
may designate them.  The special constant symbol qw is used for the value
of the function defined by a LISP program in case the computation doesn't
terminate; its use requires a justification that will be given later.

	Each function or predicate constant symbol is assigned a
function or predicate on the domain  We will normally assign to the
basic LISP function and predicate symbols the corresponding basic LISP
functions and predicates.  A predicate that has been designated as a sort
is assigned the
characteristic predicate of the subdomain consisting of all the elements of
that sort.  (The characteristic
predicate of a set is the predicate that is qtrue exactly on elements of the set).
We require that the subdomain corresponding to a sort be non-empty.
Thus ⊗isesexp is assigned to the characteristic predicate of the subdomain of 
extended S-expressions, ⊗issexp is assigned the 
characteristic predicate of the subdomain of S-expressions, and ⊗islist 
is assigned the characteristic predicate for the subdomain of lists.
Function and predicate parameter symbols do not get assigned any meaning.
Their use is mainly in writing axiom schemata from which an axiom can
be obtained by substituting an actual function or predicate expression 
for the parameter.  

	Each variable appearing free in a formula is assigned an element of the 
domain.  A general variable maybe assigned any element of the domain.  A sorted 
variable is assigned an element from the corresponding subdomain.
This collection of assignments constitutes 
an interpretation, and the truth of a formula is relative to the
interpretation.

	The truth of a formula is determined from the values of its
constituents by evaluating successively larger subexpressions.  The
rules for handling functions and predicates, conditional expressions,
equality, and Boolean expressions are exactly the same as those we
have used in the previous chapters.  We need only explain quantifiers
and lambdas.

	⊗⊗[∀x%41%*_..._x%4n%*:_s]⊗ is qtrue if and only if ⊗s is 
qtrue for ⊗all allowed assignments of elements of the domain to the ⊗⊗x⊗'s.  
An assignment is allowed if the variable is general or if it is sorted and the
assignment is to an element of the corresponding subdomain.
If ⊗s has free variables that are not among the ⊗⊗x⊗'s, then the
truth of the formula depends on the values assigned to these remaining
free variables.  ⊗⊗[∃x%41%*_..._x%4n%*:_s]⊗ is qtrue if and only if ⊗s is
qtrue for ⊗some allowed assignment of elements of the domain to
the ⊗⊗x⊗'s.  Free variables are handled just as before.

	⊗⊗[λx%41%*_..._x%4n%*:_e]⊗ is assigned a function or predicate according
to whether ⊗e is a term or a formula.  The value of
⊗⊗[λx%41%*_..._x%4n%*:_e][t%41%*,...,t%4n%*]⊗ is obtained by evaluating the 
⊗⊗t⊗'s and using these values as values of the ⊗⊗x⊗'s in the
evaluation of ⊗e.  If ⊗e has free variables in addition to the ⊗⊗x⊗'s,
the function or predicate assigned will depend on them too.

	To see how sorts actually work, we will examine some typical sentences.
Assume ⊗x is of sort ⊗issexp and ⊗XX is a general variable.
Then the sentence ⊗⊗∀x:_[¬qat x_⊃_x_=_qa x_._qd x]⊗ has the same truth value 
as ⊗⊗∀XX:_[issexp_XX_⊃_[¬qat XX_⊃_XX_=_qa XX_._qd XX]]⊗ and
the sentencc ⊗⊗∃x:_¬qat x⊗ has the same truth value as
 ⊗⊗∃XX:_[issexp_XX_∧_¬qat XX]⊗.  This  follows from the rules
forming interpretations and evaluating quantified expressions.
The formula ⊗⊗∃x:_issexp_x⊗ is guaranteed to be qtrue since
we have required that the subdomain corresponding to ⊗issexp (or any sort)
is non-empty.


	Those who are familiar with the lambda calculus should note
that λ is being used here in a very limited way.  Namely, the variables
in a lambda-expression take only elements of the domain as values,
whereas the essence of the lambda calculus is that they take arbitrary
functions as values.  We may call these restricted lambda expressions
⊗first ⊗order ⊗lambdas.  
.ss Conditional Expressions.


	All the properties we shall use of conditional forms follow
from the relation

!eqncond1 ⊗⊗⊗[s ⊃ [qif s qthen a qelse b] = a] ∧ [¬s ⊃ [qif s qthen a qelse b] = b] ⊗.

	It is worthwhile to list separately some properties
of conditional terms.  First we have the obvious
.begin nofill group

⊗⊗⊗[qif T qthen a qelse b] = a		⊗
!eqncond2 
⊗⊗⊗[qif F qthen a qelse b] = b .		⊗
.end

Next we have a ⊗distributive ⊗law for functions applied
to conditional terms, namely

!eqncond4 ⊗⊗⊗f[qif s qthen a qelse b] = qif s qthen f[a] qelse f[b] ⊗.

This applies to predicates as well as functions and can also be used
when one of the arguments of a function of several arguments is a
conditional term.  It also applies when one of the terms of
a conditional term is itself a conditional term.

Thus
.begin nofill group

!eqncond5 ⊗⊗⊗qif [qif r qthen s%41%* qelse s%42%*] qthen a qelse b =					⊗
⊗⊗⊗qif r qthen [qif s%41%* qthen a qelse b] qelse [qif s%42%* qthen a qelse b]⊗
and
⊗⊗⊗qif r qthen [qif s qthen a qelse b] qelse c =						⊗
!eqncond6 ⊗⊗⊗qif s qthen [qif r qthen a qelse c] qelse [qif r qthen b qelse c] .		⊗
.end
	When the expressions following qthen and qelse are
sentences, then the conditional term can be replaced by a sentence
according to

!eqncond7 ⊗⊗⊗[qif r qthen s%41%* qelse s%42%*] ≡ [r ∧ s%41%*] ∨ [¬r ∧ s%42%*] ⊗.

These two rules permit eliminating conditional terms from sentences
by first using distributivity to move the conditionals
to the outside of any functions and then replacing the conditional
term by a Boolean expression.

	Note that the elimination of conditional terms may increase
the size of a sentence, because ⊗r occurs twice in the right
hand side of the above equivalence.  In the most unfavorable case,
⊗r is dominates the size of the expression so that writing it
twice almost doubles the size of the expression.

	Suppose that ⊗a and ⊗b in ⊗⊗qif_s_qthen_a_qelse_b⊗
are expressions that may contain the sentence ⊗s.  Occurrences
of ⊗s in ⊗a can be replaced by T, and occurrences of ⊗s in
⊗b can be replaced by F.  This follows from the fact that
⊗a is only evaluated if ⊗s is true and ⊗b is evaluated only
if ⊗s is false.

	This leads to a strengthened form of the law of replacement
of equals by equals.  The ordinary form of the law says that if
we have ⊗⊗e_=_e'⊗, then we can replace any occurrence of ⊗e in 
an expression by an occurrence of ⊗e'.  However, if we want
to replace ⊗e by ⊗e' within ⊗a within
⊗⊗qif_s_qthen_a_qelse_b⊗,
then we need only prove ⊗⊗s_⊃_e_=e'⊗, and to make the replacement
within ⊗b we need only prove ⊗⊗¬s_⊃_e_=_e'⊗.

	More facts about conditional terms are given in [McCarthy 1963]
including a discussion of canonical forms that parallels the canonical
forms of Boolean terms.  Any question of equivalence of conditional
terms is decidable by truth tables analogously to the decidability of
propositional sentences.
.ss Lambda-expressions.

	The only rule required for handling lambda-expressions
in first order logic is called ⊗lambda-conversion.  Essentially it is

⊗⊗⊗[λx: e][a] =⊗ < the result of substituting ⊗a for ⊗x in ⊗e >.

As examples of this rule, we have

⊗⊗⊗[λx: qa x . y][u . v] = [qa [u . v]] . y .		⊗

However, a complication requires modifying the rule.  Namely,
we can't substitute for a variable ⊗x an expression ⊗e that has a free variable
⊗y into a context in which ⊗y is bound.  Thus it would be
wrong to substitute ⊗⊗y_+_z⊗ for ⊗x in ⊗⊗∀y:_[x_+_y_=_z]⊗ or into
the term ⊗⊗[λy:_x_+_y][u_+_v]⊗.  Before doing the substitution, the
variable ⊗y would have to be replaced in all its bound occurrences by
a fresh variable.

	Lambda-expressions can always be eliminated from sentences and
terms by lambda-conversion, but the expression may increase greatly
in length if a lengthy term replaces a variable that occurs more than
once in ⊗e.  It is easy to make an expression of length proportional to ⊗n whose
length is proportional to 2%5n%* 
after conversion of its ⊗n nested lambda-expressions.
For example 

	
⊗⊗⊗λx%41%*: [x%41%*.x%41%*][ ... [λx%4n%*: [x%4n%*.x%4n%*][$$A$]] ... ]⊗

becomes 

	$$(A . A)$,

	$$((A . A) . (A . A))$,

or

	$$((((A . A) . (A . A)) . ((A . A) . (A . A))) . ((A . A) . (A . A)) . ((A . A) . (A . A))))$

for ⊗n = 1, 2, or 4 respectively.
.ss First Order Axioms for LISP.
 
	We are interested in the first order theory of LISP.  That is, we are
interested  in determining what formulas involving variables ranging over
lists and S-expressions and function and predicate symbols representing LISP
functions and predicates are qtrue.  In order to describe this theory we 
represent the algebraic facts about lists, S-expressions and basic LISP 
functions and predicates by axioms (sentences of the theory which
we assume to be qtrue).  The axioms are given names either individually or in
small groups. To refer to the second axiom in a group named $AXNAME we write
$AXNAME2.  

.turnon "∂"

.bb Sorts and variables.

	Before stating the axioms we list the sorts
and give the variables which range over these sorts.  The statement ⊗⊗x_ε_issexp⊗
means that the variable ⊗x ranges over the subdomain with characteristic predicate
⊗issexp.  
.nofill

$SORTS:	        ⊗isesexp, ⊗issexp, ⊗islist 

$VARIABLES:     
        $GENERAL:       ∂(24)⊗⊗XX, YY, ZZ⊗

        $SORTED:        ∂(24)⊗⊗X, Y, Z⊗	ε ⊗isesexp 
                        ∂(24)⊗⊗x, y, z⊗	ε ⊗issexp 
                        ∂(24)⊗⊗u, v, w⊗	ε ⊗islist   

.fill
	Note that from these declarations we can show such facts as ⊗⊗∀x:_issexp_x⊗.
To see this, we observe that this sentence has the same truth value as
⊗⊗∀X:_issexp_X_⊃_issexp_X⊗ which clearly is qtrue.

.bb Domain facts.

	The first group of axioms give facts about the various sorts(subdomains) and 
their relations.

$ESEXP:         ∂(16)⊗⊗∀x: isesexp x⊗

                ∂(16)⊗⊗isesexp qw⊗

                ∂(16)⊗⊗∀X: issexp X ∨ X = qw⊗

$SEXP:          ∂(16)⊗⊗∀u: issexp u⊗

                ∂(16)⊗⊗¬issexp qw⊗

                ∂(16)⊗⊗∀XX: qat XX ⊃ issexp XX⊗

$NIL:           ∂(16)⊗⊗islist qNIL⊗

$NULL:          ∂(16)⊗⊗∀u: [qn u ≡ u=qNIL]⊗

                ∂(16)⊗⊗∀u: [qn u ≡ qat u]⊗


.bb Function ranges.

	Next are the axioms describing the ranges of the basic LISP functions.

$CONS:          ∂(16)⊗⊗∀x y: ¬qat [x . y]⊗

                ∂(16)⊗⊗∀x y: issexp [x . y]⊗

                ∂(16)⊗⊗∀x u: islist [x . u]⊗

$CAR:           ∂(16)⊗⊗∀x: [¬qat x ⊃ issexp qa x]⊗

$CDR:           ∂(16)⊗⊗∀x: [¬qat x ⊃ issexp qd x]⊗

                ∂(16)⊗⊗∀u: [¬qn u ⊃ islist qd u]⊗

.bb  Function relations.
	
	Finally we have the axioms describing the relations among the basic LISP functions.

$CAR-CONS:      ∂(16)⊗⊗∀x y: qa [x . y] = x⊗

$CDR-CONS:      ∂(16)⊗⊗∀x y: qd [x . y] = y⊗

$CONSTRUCT:     ∂(16)⊗⊗∀x: [¬qat x ⊃ [qa x . qd x] = x]⊗   


	An alternate form of $CONSTRUCT which we will find useful is

$EQ-SEXP:       ∂(16)⊗⊗∀x y: [[¬qat x ∧ ¬qat y] ⊃ [qa x = qa y ∧ qd x = qd y ≡ x = y]] ⊗.
 
.turnoff

	These axioms are analogous to the algebraic part of Peano's
axioms for the non-negative integers.  The analogy can be made clear
if we write Peano's axioms using ⊗n' for the successor of ⊗n and
⊗⊗n⊗%5-%* for the predecessor of ⊗n.  Peano's algebraic axioms
then become

⊗⊗⊗∀n: n' ≠ 0 ,				⊗

⊗⊗⊗∀n: (n')%5-%* = n ,		  	    ⊗

and

⊗⊗⊗∀n: n ≠ 0 ⊃ (n%5-%*)' = n .		  ⊗

Lists can model integers if we identify 0 with qNIL and assume that
there is only one object (say qNIL again) that can serve as a list element.
Then ⊗⊗n'_=_cons[qNIL,n]⊗, and ⊗⊗n%5-%*_=_qd n⊗.

.ss Axiom Schemas of Induction.


	Clearly S-expressions and lists satisfy the axioms given for them,
but unfortunately these algebraic axioms are insufficient to
characterize them.  For example, consider a domain of one element
⊗a satisfying

⊗⊗⊗qa a = qd a = a . a = a .		⊗

It satisfies the algebraic axioms for S-expressions.  We can exclude
it by an axiom ⊗⊗∀x: [qa x ≠ x]⊗, but this won't exclude other
circular list structures that eventually return to the same element
by some qqa-qqd chain.  Actually we want to exclude all infinite
chains, because most LISP programs won't terminate unless every
qqa-qqd chain eventually terminates in an atom.  This cannot be
done by any finite set of axioms.


	
	In order to exclude circular and infinite list structures we need
axiom schemas of induction analogous to Peano's for the integers.  Peano's
induction schema is ordinarily written

⊗⊗⊗P(0) ∧ ∀n: (P(n) ⊃ P(n')) ⊃ ∀n: P(n) .⊗

Here ⊗P(n) is an arbitrary predicate of integers, and we get particular
instances of the schema by substituting particular predicates.
It is called an axiom schema rather than an axiom, because we consider
the schema, which is not properly a sentence of first order logic, as
standing for the infinite collection of axioms that arise from it by
substituting all possible predicates for ⊗P.

	The S-expression induction schema is

$SEXPINDUCTION:	   ⊗⊗∀x: [qat x ⊃ qP x] ∧ ∀x: [¬qat x ∧ qP qa x ∧ qP qd x ⊃ qP x] ⊃ ∀x: qP x ⊗.


	The corresponding axiom schema for lists is

$LISTINDUCTION:	   ⊗⊗∀u: [qn u ⊃ qP u] ∧ ∀u: [¬qn u ∧ qP qd u ⊃ qP u] ⊃ ∀u: qP u ⊗.

Here qP is a predicate variable.

	These schemas are called principles of ⊗structural ⊗induction, 
since the induction is on the structure of the entities involved. Other schemas
derived from principles of ⊗structural ⊗induction are possible and the best schema 
to use depends stongly on the problem at hand.  Some examples will be given in a 
later section.

	Even the axiom schemas don't assure us that the only domain
satisfying the axioms is that of the integers or the S-expressions as
the case may be.  Any first order theory whose axioms
can be given effectively admits the so-called ⊗non-standard_models.  
However, it seems likely that the non-standard models of S-expressions,
like the non-standard models of integers, will agree with the standard
model for sentences of practical interest.
.ss A Simple Example. 

	In order to complete our description of the first order theory of LISP
we need to be able to represent facts about recursively defined LISP functions.
Given a recursive function definition we can form the ⊗functional_equation 
by replacing the "←" in the recursive function definition by "=" and universally
quantifying over the argument variables. In the case of ⊗append which is defined by

⊗⊗⊗u * v ← qif qn u qthen v qelse qa u . [qd u * v]⊗

the corresponding functional equation is

$APPEND:		⊗⊗∀u v: [u * v = qif qn u qthen v qelse qa u . [qd u * v]] ⊗.

Sometimes the functional equation  characterizes the function completely.
For this to be the case we need to
know that a function satisfying the equation exists and that it is unique. This
essentially reduces to showing that the function is total.  If the function is
not total then we need the additional information provided by the 
⊗minimiztion_schema.   This is justified by the semantics of LISP programs
based on the use of functionals and fixedpoints.  Before proceeding with
a more detailed discussion of these matters an example is in order.

	For the remainder of this section we will 
show how to use the axiom $APPEND together with the LISP
axioms to prove some properties of ⊗append.  In particular we will show

$NIL-APPEND:		⊗⊗∀v: qNIL * v = v⊗

$ISTOT-APPEND:		⊗⊗∀u v: islist [u * v]⊗

$CAR-APPEND:		⊗⊗∀u v: [¬qn u ⊃ qa [u * v] = qa u]⊗

$CDR-APPEND:		⊗⊗∀u v: [¬qn u ⊃ qd [u * v] = [qd u] * v]⊗

$NOTNUL-APPEND:		⊗⊗∀u v: [[¬qn u ∨ ¬qn v] ⊃ ¬qn [u * v]]⊗

$AASOC-APPEND:		⊗⊗∀u v w: [u * v] * w = u * [v * w]⊗

	First we prove $NIL-APPEND.  By $APPEND and the axiom $NIL we have

⊗⊗⊗qNIL * v = qif qn qNIL qthen v qelse qa u . [qd u * v]⊗

and by $NULL this simplifies to  ⊗⊗qNIL * v = v⊗  as desired.

	Next we prove $ISTOT-APPEND, i.e. that ⊗append is total.  For this we use
$LISTINDUCTION with 

⊗⊗⊗qP u ≡ ∀v: islist [u * v]		⊗

obtaining the induction axiom

.NOFILL

⊗⊗⊗[∀u: [qn u ⊃ ∀v: islist [u * v]] ∧ 					⊗
⊗⊗⊗∀u: [[¬qn u ∧ ∀v: islist [qd u * v]] ⊃ ∀v: islist [u * v]]]⊗
⊗⊗⊗⊃ ∀u v: islist [u * v] .				⊗
.FILL

The proof then breaks into two steps corresponding to the cases ⊗⊗qn u⊗ and
⊗⊗¬qn u⊗. In the first case we must show

⊗⊗⊗∀u: [qn u ⊃ ∀v: islist [u * v]]	⊗

which follows directly from $APPEND and $SORTED. 
In the second case we must show 

⊗⊗⊗∀u: [[¬qn u ∧ ∀v: islist [qd u * v]] ⊃ ∀v: islist [u * v]] ⊗.

To do this we assume 

⊗⊗⊗¬qn u ∧ ∀v: islist [qd u * v] .	⊗

Then by $NULL, $CAR we have ⊗⊗issexp qa u⊗ and so by $CONS3 we have

⊗⊗⊗islist [qa u . [qd u * v]] .		⊗

From this and $APPEND, since we are in the case ⊗⊗¬qn u⊗, it follows that

⊗⊗⊗islist [u * v] .		⊗

$ISTOT-APPEND follows immediately from these two steps and the induction axiom.


	We now prove $CAR-APPEND.  From $APPEND we have 

⊗⊗⊗¬qn u ⊃ [u * v = qa u . [qd u * v]] .⊗

Now we use $CAR-CONS and obtain

⊗⊗⊗¬qn u ⊃ [qa [u * v] = qa u]		⊗

To justify using $CAR-CONS we need ⊗⊗issexp qa u⊗, ⊗⊗islist qd u⊗ and 
⊗⊗islist [qd u * v]⊗ under the assumption that ⊗⊗¬qqn_u⊗. These follow from
($NULL, $CAR), $CDR2; and $ISTOT-APPEND respectively.
$CDR-APPEND is proved similiarly with $CDR-CONS in place of $CAR-CONS. 


	To prove $NOTNUL-APPEND we note first that

⊗⊗⊗¬qn u ⊃ ¬qn [u * v]			⊗

follows from $APPEND, $NULL, $CAR, $CDR2, $ISTOT-APPEND, and $CONS1.  Second we have

⊗⊗⊗[qn u ∧ ¬qn v] ⊃ ¬qn [u * v]		⊗

by $APPEND.  Combining these two we have the desired result.

	
	Finally we prove $ASSOC-APPEND.  Again we use $LISTINDUCTION, this time with

⊗⊗⊗qP u ≡ ∀v w: [u * v] * w = u * [v * w] ⊗.

First we show 

⊗⊗⊗∀u: [qn u ⊃ ∀v w: [u * v] * w = u * [v * w]] ⊗.

Assuming ⊗⊗qn u⊗ we have by $APPEND that

⊗⊗⊗[u * v] * w = v * w			⊗

and by $APPEND and $ISTOT-APPEND that 

⊗⊗⊗u * [v * w] = v * w			⊗

proving the first step.

The second step is to show that

⊗⊗⊗∀u: [[¬qn u ∧ ∀v w: [qd u * v] * w = [qd u] * [v * w]] ⊃ ∀v w: [u * v] * w = u * [v * w]] ⊗.

We do this by assuming the lefthand side of the implication and proving a chain
of equalities which will prove the righthand side of the implication.
By $APPEND, $NOTNUL-APPEND and $ISTOT-APPEND we have

⊗⊗⊗[u * v] * w = qa [u * v] . [qd [u * v] * w]⊗

and by $CAR-APPEND and $CDR-APPEND 

⊗⊗⊗qa [u * v] . [qd [u * v] * w] = qa u . [[qd u * v] * w] ⊗.

By assumption

⊗⊗⊗qa u . [[qd u * v] * w] = qa u . [[qd u] * [v * w]] ⊗.

Finally by $APPEND and $ISTOT-APPEND since we are in the case ⊗⊗¬qn u⊗

⊗⊗⊗qa u . [[qd u] * [v * w]] = u * [v * w] ⊗.

Combining these two steps with the induction axiom we have the desired result.


	In the above proofs we have been particularly careful with details
such as showing ⊗⊗islist x⊗ where ⊗x is an expression to be substituted for 
⊗u in some sentence. The proofs are in fact fairly close to the formal proofs
given in  Appendix {SECTION FOL}.  In later examples we shall be more brief as the reader
will be expected to be able to fill in the details.
.ss Pseudo-logic.
 
	In this section we give a method for handling recursively defined predicates.
Consider the recursive program

⊗⊗⊗occur[x, y] ← [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]⊗.

If we were to treat this program in a manner analogous to the functional equation
method described in the last section, we would represent the predicate ⊗occur 
by the sentence

⊗⊗⊗∀x y: [occur[x, y] ≡ [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]]⊗.

However, in order to justify this representation we would have to use
some kind of logic of partial predicates, because we could not be sure
in advance that ⊗occur is total, and honest predicates cannot take the
value qw; they can only be true or false.

	Instead, we introduce a domain TV of truth values consisting
of the elements $TT and $FF and having characteristic predicate ⊗istv. The 
extension, TV%5+%*, of TV we shall call ETV. It consists of the elements $TT, $FF, 
and qw and has characteristic predicate ⊗isetv.  By identifying $TT and $FF with
appropriate LISP atoms TV could be considered as a subdomain of SE.  For our
purposes it makes no difference.  We define pseudo-logical operators (⊗nnot, 
⊗aand, ⊗oor) to imitate the logical operators (¬, ∧, ∨) and pseudo-predicates
(⊗eeq, ⊗aatom) to imitate the basic LISP predicates (=, qqat). 

	Now we can imitate the predicate ⊗occur by the recursive program

⊗⊗⊗occura[x, y] ← [x eeq y] oor [nnot aatom y aand [occura[x, qa y] oor occura[x, qd y]]]⊗

which has the functional equation

⊗⊗⊗∀x y: [occura[x, y] = [x eeq y] oor [nnot aatom y aand [occura[x, qa y] oor occura[x, qd y]]]]⊗.

Using this equation and the S-expression induction axiom we can show

⊗⊗⊗∀x y: istv occura[x, y]			⊗

which is the statement that occura is total.  If we define ⊗occur by

⊗⊗⊗∀x y: [occur[x, y] ≡ occura[x, y] = $$TT$]	⊗  

then we can prove the original sentence proposed for representing ⊗occur. 

.bb ETV axioms

	We now give the axioms for extended truths values needed to make the above
arguments and similar ones work.  First the axioms describing the domains TV and ETV.
.begin nofill

$TVSORTS:  	⊗etv, ⊗tv 

$VARIABLES:  
	$SORTED:  	⊗⊗P, Q  ε etv⊗ 
			    ⊗⊗p, q 	ε tv⊗
.end

$B2: 	⊗⊗∀p: isetv p⊗  

$B3: 	⊗⊗isetv qw ∧ istv $TT ∧ istv $FF ⊗

$B4: 	⊗⊗∀P: [P = $TT ∨ P = $FF ∨ P = qw]⊗

$B5: 	⊗⊗∀p: [p = $TT ∨ p = $$FF$]⊗

$B6: 	⊗⊗$TT ≠ $FF ∧ $TT ≠ qw ∧ $FF ≠ qw⊗

	Next the axioms defining the functions on ETV corresponding to the
pseudo-logical operators and pseudo-predicates.

$B7: 	⊗⊗∀P: [nnot P = qif [P = qw] qthen qw qelse qif [P = $$TT$] qthen $FF qelse $$TT$]⊗

$B8: 	⊗⊗∀P Q: [P aand Q = qif [P = qw] qthen qw qelse if [P = $$TT$] qthen Q qelse $$FF$]⊗

$B9: 	⊗⊗∀P Q: [P oor Q = qif [P = qw] qthen qw qelse qif [P = $$TT$] qthen $TT qelse Q]⊗

$B10: 	⊗⊗∀X Y: [X eeq Y] = qif [¬issexp X ∨ ¬issexp Y] qthen qw qelse qif [X = Y] qthen $TT qelse $$FF$]⊗

$B11: 	⊗⊗∀X: [aatom X = qif [¬issexp X] qthen qw qelse qif qat x qthen $TT qelse $$FF$]⊗

	Finally a conditional function which takes elements of ETV as its first argument.

$B12: 	⊗⊗∀P X Y: [iif[P, X, Y] = qif [P = qw] qthen qw qelse qif [P = $$TT$] qthen
X qelse Y]⊗

.bb ETV lemmas

	We now give some lemmas which show that the pseudo- operators and predicates
behave as advertised.  First we need to know that the functions map into ETV.

$ETVNNOT: 		⊗⊗∀P: isetv nnot P⊗

$ETVAAND: 		⊗⊗∀P Q: isetv [P aand Q]⊗

$ETVOOR: 		⊗⊗∀P Q: isetv [P oor Q]⊗

$ETVEEQ: 		⊗⊗∀X Y: isetv [X eeq Y]⊗

$ETVAATOM: 		⊗⊗∀X: isetv aatom X⊗

	These lemmas are all a direct consequence of the function definitions and 
the axioms $SORTED, $B2 and $B3. 

	Next are some lemmas stating that the functions defined above are total
when restricted to the domains TV or SE as appropriate.

$TVNNOT: 		⊗⊗∀p: istv nnot p⊗

$TVAAND: 		⊗⊗∀p q: istv [p aand q]⊗

$TVOOR: 		⊗⊗∀p q: istv [p oor q]⊗

$TVEEQ: 		⊗⊗∀x y: istv [x eeq y]⊗

$TVAATOM:  		⊗⊗∀x: istv atom x⊗

	These lemmas follow from the function definitions and the axioms $SORTED, 
$B3, $B5 and $B6.   

	Next are some lemmas which show that the functions do indeed imitate their
logical counterparts.

$EQNNOT: 		⊗⊗∀p: [nnot p = $TT ≡ ¬[p = $$TT$]]⊗

$EQAAND: 		⊗⊗∀p q: [p aand q = $TT ≡ p = $TT ∧ q = $$TT$]⊗

$EQOOR: 		⊗⊗∀p q: [p oor q = $TT ≡ p = $TT ∨ q = $$TT$]⊗

$EQEEQ: 		⊗⊗∀x y: [x eeq y = $TT ≡ x = y]⊗

$EQAATOM: 		⊗⊗∀x: [aatom x = $TT ≡ qat x]⊗

	These lemmas can all be proved by simple case analysis.  We prove $EQAAND
and $EQEEQ as examples.  By $SORTED, $B5, $B6, and $B8  we have 

⊗⊗⊗p aand q = qif [p=$TT] qthen q qelse $FF	⊗

and $EQAAND follows immediately using $B6.  By $SORTED and $B10 

⊗⊗⊗x eeq y = qif [x = y] qthen $TT qelse $FF	⊗

and $EQEEQ follows using $B6. 

	Finally we give some lemmas that will be useful in later examples.

$TVNOTATM:		⊗⊗∀x y: istv [nnot aatom x aand nnot aatom y]⊗

$EQNOTATM:		⊗⊗∀x y: [[nnot aatom x aand nnot aatom y] = $TT ≡ [¬qat x ∧ ¬qat y]]⊗

	$TVNOTATM follows from $TVNNOT, $TVAATOM, and $TVAAND.  $EQNOTATM follows from
$EQAAND and ⊗⊗∀x:_nnot_aatom_x_=_$$TT$_≡_¬qat x⊗.  The latter follows from $TVAATM, 
$EQNNOT and $EQAATOM.  

$POORF:			⊗⊗∀P: [P oor $FF = P]⊗

$FAANDQ:		⊗⊗∀Q: [$FF aand Q = $$FF$]⊗

	$POORF follows from $B9 by case analysis using $B4 and $B6.  $FAANDQ follows
 by simplification of $B8 using $B6.  


	A formal proof of many of the above lemmas is included in  
Appendix {SECTION FOL}.  

.cb Exercise.

	Prove the statements made about ⊗occur and ⊗occura.  Namely show


⊗⊗⊗∀x y: istv occura[x, y]			⊗

and

⊗⊗⊗∀x y: [occur[x, y] ≡ [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]]⊗.

using the definitions


⊗⊗⊗∀x y: [occura[x, y] = [x eeq y] oor [nnot aatom y aand [occura[x, qa y] oor occura[x, qd y]]]]⊗ 

and

⊗⊗⊗∀x y: [occur[x, y] ≡ occura[x, y] = $$TT$].	⊗  
.ss An Extended Example.
 
	As a non trivial application of the techniques described in the previous
sections, we will give a proof of correctness of the predicate ⊗samefringe 
which has been proposed as a solution of the SAMEFRINGE problem.  This is the
problem of determining whether or not two S-expressions have the same fringe
using a minimum of space.  (We will be concerned only with the correctness of
⊗samefringe since the efficiency is not an ⊗extensional property).  

	The fringe of an S-expression, ⊗x, is a list of atoms in the order that
they occur in ⊗x.  Thus the fringe of $A is $(A) and the fringe of
$$((A_._B)_._(C_._D))$ is $$(A_B_C_D)$.  The LISP program for computing the
fringe of an S-expression is

!fcnfringe&sf ⊗⊗⊗fringe x ← qif qat x qthen <x> qelse [fringe qa x] * [fringe qd x]⊗

The predicate ⊗samefringe is computed by the LISP program

!fcnsamefringe&  ⊗⊗⊗samefringe[x, y] ← x = y ∨ [¬qat x ∧ ¬qat y ∧ same[gopher x, gopher y]]⊗

where

!fcnsame&  ⊗⊗⊗same[x, y] ← qa x = qa y ∧ samefringe[qd x, qd y]⊗

and 

!fcngopher&  ⊗⊗⊗gopher x ← qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]⊗


Using the method of the previous section we define an imitation of ⊗samefringe by
.begin nofill 

⊗⊗⊗samefringea[x, y] ← [x eeq y] oor [[nnot aatom x aand nnot aatom y]⊗
!fcnsamefringea&  ⊗⊗⊗		aand samea[gopher x, gopher y]]⊗
.end

where

!fcnsamea&  ⊗⊗⊗samea[x, y] ← [qa x eeq qa y] aand samefringea[qd x, qd y]⊗

Thus we have the functional equations
.begin nofill

$FRINGE:	⊗⊗∀x: [fringe x = qif qat x qthen <x> qelse [fringe qa x] * [fringe qd x]]⊗


$SAMEFRINGEA:	⊗⊗∀x y: [samefringea[x, y] = [x eeq y] oor [[nnot aatom x aand nnot aatom y]⊗
							⊗⊗aand samea[gopher x, gopher y]]]⊗

$SAMEA:		⊗⊗∀x y: [samea[x, y] = [qa x eeq qa y] aand samefringea[qd x, qd y]]⊗

$SAMEFRINGE:	⊗⊗∀x y: [samefringe[x, y] ≡ samefringea[x, y] = $$TT$]⊗

$SAME:		⊗⊗∀x y: [same[x, y] ≡ samea[x, y] = $$TT$]⊗

$GOPHER: 	⊗⊗∀x: [gopher x = qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]]⊗
.end
	In order to prove that ⊗samefringea is total we will need the
fact that ⊗samea maps into ETV.  This is because in the case ⊗x is an atom or ⊗y 
is an atom we must have ⊗⊗isetv_samea[gopher_x,_gopher_y]⊗ in order to use the
definition of ⊗aand even though the actual value is irrelevant. There are several
ways to do this.  One would be to define ⊗gopher of an atom to be qw, and have
an axiom stating that ⊗samea produces qw if either argument is qw.  Another
is to take as part of the definition of ⊗samea that it maps into ETV, without
stating for what arguments it actually produces qw.  We have chosen the latter
option as it seems cleaner.  Thus we add the axiom

$ETVSAMEA:	⊗⊗∀X Y  isetv samea[X, Y]⊗

	The goal is to prove the following three statements:

$THM1:		⊗⊗∀x y: istv samefringea[x, y]⊗

$THM2:		⊗⊗∀x y: [samefringe[x, y] ≡ [x = y] ∨ [[¬qat x ∧ ¬qat y] ∧ same[gopher x, gopher y]]⊗

$THM3:		⊗⊗∀x y: [samefringe[x, y] ≡ fringe x = fringe y]⊗

	$THM1 says that ⊗samefringea is total, $THM2 says that ⊗samefringe as defined
via its imitatiom satisfies the intended equivalence, and $THM3 says that ⊗samefringe is
correct.

	Due to the complicated form of the recursion defining ⊗samefringe, simple
S-expression induction is not adequate to prove the above theorems.  Therefore 
if we wish to carry out the proof by structural induction we must find an
axiom schema appropriate for the problem.  One way is to use induction
on the size of the S-expressions involved.  The size of an S-expression
⊗x is the number of atoms occuring in ⊗x and is computed by the LISP program 

!fcnsize&  ⊗⊗⊗size x ← qif qat x qthen 1 qelse size qa x + size qd x⊗

⊗size provides a mapping of S-expressions into the domain of natural numbers
and allows us to transform the problem into one of natural number induction.
In particular we will take for the axiom schema, the course of values induction
schema

$NUMBINDUCTION:		⊗⊗∀n: [∀m: [m < n ⊃ qP m] ⊃ qP n] ⊃ ∀n: qP n⊗

with

⊗⊗⊗qP n ≡ ∀x y: [size x + size y = n ⊃ THM[x, y]]⊗

where 

$THM:			⊗⊗∀x y: [THM[x, y] ≡ THM1[x, y] ∧ THM2[x, y] ∧ THM3[x, y]]⊗.

	In order to use the $NUMBINDUCTION  axiom we will need the functional
equation for ⊗size and some properties of the natural numbers.  The characteristic
predicate of the domain of natural numbers is ⊗natnum and we add to our list of
axioms the following:


$NUMSORTS:      ⊗natnum

$VARIABLES:     ⊗⊗k, l, m, n ε natnum⊗

$ONE:		⊗⊗natnum 1⊗

$ISTOT-PLUS:	⊗⊗∀m n: natnum [m + n]⊗

$ASSOC:		⊗⊗∀l m n: l + [m + n] = [l + m] + n⊗

$ORDER-PLUS:	⊗⊗∀k l m n: [[k < l ∧ m < n] ⊃ k + m < l + n]⊗

$ORDER:		⊗⊗∀n: n < 1 + n⊗

$SIZE: 		⊗⊗∀x: [size x = qif qat x qthen 1 qelse size qa x + size qd x]⊗


Here we have not attempted to axiomatize the natural numbers, but simply have
taken as axioms those properties needed for the present problem.  


	Now to proceed with the proof.  In addition to the lemmas  about
⊗append and the ETV lemmas proved in earlier sections, we will need some lemmas
about ⊗gopher, ⊗fringe, ⊗size and combinations thereof. They are

$GOOD-GOPHER: 	⊗⊗∀x: [¬qat x ⊃ [issexp gopher x ∧ issexp qa gopher x ∧ issexp qd gopher x]]⊗

$GOOD-FRINGE:	⊗⊗∀x: [issexp fringe x ∧ ¬qat fringe x]⊗

$FRINGE-ATM:	⊗⊗∀x y: [[qat x ∨ qat y] ⊃ [fringe x = fringe y ≡ x = y]]⊗

$FRINGE-GOPHER:	⊗⊗∀x: [¬qat x ⊃ [qa fringe x = qa gopher x] ∧ [qd fringe x = fringe qd gopher x]]⊗

$ISTOT-SIZE:	⊗⊗∀x: natnum size x⊗

$SIZE-GOPHER:	⊗⊗∀x y: [[¬qat x ∧ ¬qat y] ⊃ [size qd gopher x +size qd gopher y] 
< [size x + size y]]⊗

	We will give only a brief indication of the proof of these lemmas.  Formal
proofs are contained in  Appendix_{SECTION FOL}.

	The key idea in proving things about
⊗gopher is to first prove properties of ⊗⊗gopher[x_._y]⊗ as gopher is only
defined for non atoms and every non atom can be expressed as ⊗⊗x_._y⊗ for suitable
⊗x and ⊗y. For this purpose we start with some useful facts derived from $GOPHER, 
$FRINGE, $SIZE and the LISP axioms.

$GOPHER-CONS-ATM:	⊗⊗∀x y: [qat x ⊃ gopher[x . y] = [x . y]]⊗

$GOPHER-CONS-NOTATM:	⊗⊗∀x y: [¬qat x ⊃ gopher[x . y] = gopher[qa x. [qd x . y]]]⊗

$FRINGE-CONS:		⊗⊗∀x y: [fringe[x . y] = fringe x * fringe y]⊗

$SIZE-CONS:		⊗⊗∀x y:  [size[x . y] = size x + size y]⊗

	To prove $GOOD-GOPHER first prove, by a straight forward use of 
$SEXPINDUCTION, that

		⊗⊗∀x y: [issexp gopher[x . y] ∧ ¬qat gopher[x . y]]⊗

The lemma then follows from this and the axioms $CAR, $CDR1 and $CONS1. 

	$GOOD-FRINGE folllows from  ⊗⊗∀x: [islist fringe x ∧ ¬qn fringe x]⊗ ,
$SEXP1,  and $NULL.  
The former is proved using $SEXPINDUCTION. 

	For $FRINGE-ATM we assume ⊗⊗qat x⊗ and show ⊗⊗fringe_x_=_fringe_y_≡_x_=_y⊗.
The lemma then follows from the symmetry of the occurrences of ⊗x and ⊗y.  From the
definition of ⊗fringe we have ⊗⊗fringe_x_=_<x>_=_[x_._qNIL]⊗.  If ⊗⊗qqat_y⊗ the
result follows using $EQ-SEXP.  If ⊗⊗¬qqat_y⊗ then ⊗⊗x_≠_y⊗ and 
by $EQ-SEXP we need only
prove ⊗⊗¬qqn_qqd_fringe_y⊗. But this follows from $CDR-APPEND and $NOTNUL-APPEND. 

	To prove $FRINGE-GOPHER we use the "gopher trick" again and first prove

⊗⊗⊗∀x y: [qa fringe[x . y] = qa gopher[x . y] ∧ qd fringe[x . y] = fringe qd gopher[x . y]]⊗

using $SEPXINDUCTION.  By $CAR-APPEND, $CDR-APPEND $GOOD-FRINGE and $FRINGE-CONS 
we have

⊗⊗⊗qa fringe[x . y] = qa fringe x,		⊗

and

⊗⊗⊗qd fringe[x . y] = [qd fringe x] * fringe y.	⊗

In the case ⊗⊗qat x⊗  the result follows from $NIL-APPEND, $GOPHER-CONS-ATM, 
 and ⊗⊗fringe_x_=_[x_._qNIL]⊗ .  In the case ⊗⊗¬qqat x⊗
we show

⊗⊗⊗fringe[x . y] = fringe[qa x . [qd x . y]]	⊗

using properties of ⊗append and $FRINGE-CONS.  Then the result follows from the
induction hypothesis and $GOPHER-CONS-NOTATM. 
$FRINGE-GOPHER now follows from the above using $CONSTRUCT. 

	$ISTOT-SIZE is proved by a straight forward application of $SEXPINDUCTION. 
To prove $SIZE-GOPHER we first show

⊗⊗⊗∀x y: [size qd gopher[x . y] < size[x . y]]⊗

using $SEXPINDUCTION.  In the case ⊗⊗qa x⊗ we have 

⊗⊗⊗size qd gopher[x . y] = size y⊗  and  ⊗⊗size[x . y] = 1 + size y⊗

by $SIZE, $SIZE-CONS and $GOPHER-CONS-ATM and the result follows by $ORDER.
In the case ⊗⊗¬qqat_x⊗ we show 

⊗⊗⊗size[x . y] = size[qa x . [qd x . y]]⊗

using $SIZE-CONS, $ASSOC and the LISP axioms. The result then follows from the
induction hypothesis and $GOPHER-CONS-NOTATM.  $SIZE-GOPHER now follows from
$CONSTRUCT and $ORDER-PLUS. 

	Now we are ready to prove the SAMEFRINGE theorem.  The proof is divided into 
two cases.  In the first case we assume ⊗⊗qat x ∨ qat y⊗.  Then
by the ETV lemmas

⊗⊗⊗nnot aatom x aand nnot aatom y = $FF ⊗,

by $FAANDP and $ETVSAMEA 

⊗⊗⊗$FF aand samea[gopher x, gopher y] = $FF ⊗,

and by $POORF 

⊗⊗⊗[x eeq y] oor $FF = x eeq y ⊗.

Thus by $SAMEFRINGEA we have

⊗⊗⊗samefringea[x, y] = x eeq y⊗

and $THM now follows using the ETV lemmas, $FRINGE-ATM and $SAMEFRINGE. 

	In the second case we assume ⊗⊗¬qat x ∧ ¬qat y⊗ and make use of the
$NUMBINDCTION axiom and predicate as mentioned above.  In particular we
have the induction hypothesis

⊗⊗⊗∀m: [m < n ⊃ ∀x%41%* y%41%*: [size x%41%* + size y%41%* = m ⊃ THM[x%41%*, y%41%*]] ⊗.

Taking  ⊗⊗n = size x + size y⊗, ⊗⊗m = size qd gopher x + size qd gopher y⊗,
⊗⊗x%41%*_=_qqd_gopher_x⊗ and ⊗⊗y%41%*_=_qqd_gopher_y⊗ we have by $SIZE-GOPHER 

$THMCDRGO:		⊗⊗THM[qd gopher x, qd gopher y]⊗

Assigning these values to ⊗n and ⊗m is allowed since by $ISTOT-PLUS, 
$ISTOT-SIZE and $GOOD-GOPHER the expressions satisfy ⊗natnum.  

	$THM1 now follows from $THMCDRGO, the ETV lemmas, $GOOD-GOPHER, $SAMEA 
and $SAMEFRINGEA.  $THM2 follows for the above reasons and $SAME.  By $SAMEA, 
$SAMEFRINGE, $GOOD-GOPHER, $THMCDRGO and the ETV lemmas it follows that
.NOFILL

⊗⊗⊗samea[gopher x, gopher y] = $TT ≡							⊗
⊗⊗⊗[qa gopher x = qa gopher y] ∧ [fringe qd gopher x = fringe qd gopher y]⊗.
.FILL

Using $FRINGE-GOPHER, $THM2, and $SAME we have

⊗⊗⊗samefringe[x, y] ≡ x = y ∨ [[qa fringe x = qa fringe y] ∧ [qd fringe x = qd fringe y]]⊗.

Finally $THM3 follows from $EQ-SEXP and $GOOD-FRINGE. 

	Combining the two cases and applying the induction axiom we conclude

⊗⊗⊗∀n: ∀x y: [[size x + size y] = n ⊃ THM[x, y]]⊗

and by $ISTOT-SIZE and $ISTOT-PLUS it follows that 

⊗⊗⊗∀x y: THM[x, y] .		⊗


	In the above proof we could have equally well used the predicate

⊗⊗⊗qP n ≡ ∀x y: [size x = n ⊃ THM[x, y]]⊗

since the recursive call to ⊗samefringe always reduces the size of the first
argument.

	Another version of ⊗samefringe without any auxilliary functions is

.begin nofill turnon "∂"
.n←16

∂(n)⊗⊗samefringe[x, y] ← ⊗
∂(n)⊗⊗    x = y ∨ ⊗
∂(n)⊗⊗    [¬qat x ∧ ¬qat y ∧ ⊗
!fcnsamefringe&1  ∂(n)⊗⊗        [qif qat qa x qthen [qif qat qa y qthen qa x = qa y ∧ samefringe[qd x, qd y] ⊗
∂(n)⊗⊗                             qelse samefringe[x, qaa y. [qda y . qd y]]]⊗
∂(n)⊗⊗         qelse samefringe[qaa x . [qda x . qd x], y]. ⊗
.end

Note that a recursive call to ⊗samefringe does one of the following:  

	1)  decreases  ⊗⊗size x + size y⊗

	2)  leaves  ⊗⊗size x + size y⊗ and ⊗⊗size qa x⊗ invariant and decreases ⊗⊗size qa y⊗

or

	3)  leaves  ⊗⊗sixe x + size y⊗ and ⊗⊗size qa y⊗ invariant and decreases ⊗⊗size qa x ⊗.

.TURN ON "↑[]"
This can lead to a choice of an induction axiom schema in at least two ways.
If in the $NUMBINDUCTION schema we let ⊗n and ⊗m range over all ordinals less
than a given one it becomes a schema of transfinite induction. Ordinary induction
is obtained as a special case where the bounding ordinal is qW the least transfinite
ordinal.  If we take the bounding ordinal to be qW↑[qW] then the SAMEFRINGE theorem
for the above version of ⊗samefringe can be proved using the predicate
.TURN OFF

⊗⊗⊗qP n  ≡ ∀x y: [[size x +size y]qW + size qa x + size qa y = n ⊃ THM[x, y]]⊗

(Note that THM2 will need to be modified to account for the new form of ⊗samefringe.)

	Alternately one could axiomatize the lexicographic ordering of triples
of numbers by
.NOFILL

⊗⊗⊗∀l%41%* m%41%* n%41%* l m n: [(l%41%*, m%41%*, n%41%*) < (l, m, n) ≡				⊗
⊗⊗⊗[l%41%* < l] ∨ [l%41%* = l ∧ m%41%* < m] ∨ [l%41%* = l ∧ m%41%* = m ∧ n%41%* < n]]⊗
.FILL
This ordering is well-founded (has no infinite decreasing sequences) and so we
have a schema analogous to $NUMBINDUCTION given by
.NOFILL

⊗⊗⊗∀l m n: [∀l%41%* m%41%* n%41%*: [(l%41%*, m%41%*, n%41%*) < (l, m, n) ⊃qP(l%41%*, m%41%*, n%41%*)] ⊃ qP(l, m, n)]⊗
⊗⊗⊗⊃ ∀l m n: qP(l, m, n)⊗
.FILL
The SAMEFRINGE theorem can now be proved using this schema with the predicate

⊗⊗⊗qP(l, m, n) ≡ ∀x y: [l = size x +size y ∧ m = size qa y ∧ n = size qa x ⊃ THM[x, y]]⊗
.ss Functionals and Least Fixedpoints. 

 
	Now we will describe a method for determining the function computed
by a recursive program.  This will allow us to justify the use of the 
functional equation to represent a total function.   It will also provide
a means of justifying the use of the functional equation together with
the minimization schema to represent partial functions in general.  The latter
will be discussed in a later section.

	We are interested in recursive programs of the form

⊗⊗⊗f x ← qt[f] x		⊗

where qt is a computable functional.  
A functional is a higher order function which takes functions as arguments 
as well as ordinary arguments.  The
result of applying a functional to a function is a function which is then 
applied to the rest of the arguments.
For example the LISP program ⊗mapcar defines a functional.  
We will consider functiionals  constructed using a function variable and
a set of base functions and predicates in a manner similar to the formation of
λ-expressions (but omitting quantifiers).   Functionals constructed in this 
manner are called ⊗term ⊗functionals.
In the case of LISP programs, the non-logical functions and predicates
are ⊗car, ⊗cdr, ⊗cons, ⊗atom and ⊗null.  

	For example,  for the function ⊗append the functional is

⊗⊗⊗qt = λF: λx y: [qif qn x qthen y qelse qa x . F[qd x,y]]⊗

or, using infix notation,

⊗⊗⊗qt = λOP: λx y: [qif qn x qthen y qelse qa x . [qd x OP y]]⊗.


	In order to say what function is computed by a recursive program of the form
given above we will need to introduce the concepts of ⊗partial ⊗ordering  
and of ⊗least ⊗fixedpoints.  We give here only a brief summary.  A more complete
discussion can be found in (Manna 1974, Chapter 5).

	Given a domain D, we form a domain D%5+%* by adjoining the undefined element
qw to D.  We use upper case letters to range over D%5+%* where 
the corresponding lower case letters range over D.   
A partial ordering, q≤ (read "less defined than or equal"), on D%5+%* is defined by 

⊗⊗⊗X q≤ Y ≡ X = qw ∨ X = Y ⊗. 

(Recall that a partial ordering on a set S is a relation on (S $x S) that is 
transitive, reflexive and antisymmetric.)    For example in the domain SE%5+%*
we have  qw_q≤_qNIL  and  qNIL_q≤_qNIL,  but not  qNIL_q≤_(qNIL_._qNIL).   
This partial ordering (sometimes called the "flat" partial ordering) is
indeed trivial.  A partial ordering can be represented by a diagram  in which
all elements less than but not equal to a given element are "below" that element.
For our trivial ordering the diagram has only two layers: the bottom layer
consisting of the single element qw and a top layer consisting of the rest.
Hence the name "flat".  Despite the trivial nature of this particular partial
ordering,  the concept turns out to be very useful.

	Given domains D1 and D2 and a partial function ⊗f: D1→D2, 
we extend ⊗f to a  function 
from D1%5+%* to D2%5+%* by defining ⊗⊗f_qw_=_qw⊗  and, if ⊗f is undefined for ⊗x 
in D1, then  ⊗⊗f_x_=_qw⊗. (Note that we use the same symbol to denote the
undefined element regardless of domain. We shall also use this symbol to denote
a totally undefined function.  Context will make it clear what is 
being denoted by qw.)  
Other extensions are possible but we will not consider them.  We will not 
distinguish between a function and its extension as we are considering only one
extension.
We "lift" the partial orderings on D1%5+%* and D2%5+%* to the set of 
partial functions from D1%5+%* to D2%5+%* by defining

⊗⊗⊗f q≤ g ≡ ∀x in D1: f x q≤ g x ⊗.


For example if D1 and D2 are the domain SE,

⊗⊗⊗f%41%* = λx: [qif qat x qthen x qelse qw]⊗

and 

⊗⊗⊗f%42%* = λx: [qif qat x qthen x qelse qif qat qa x qthen qa x qelse qw] ⊗.

then ⊗⊗f%41%* q≤ f%42%* ⊗.

	The partial ordering on the function domains is not as trivial as that on
the underlying domains but it is still very easy to work with.  A useful
concept here it that of ⊗lub (least upper bound to be precise).  
⊗lub acts on sets of functions and produces the least function in the domain
that contains (or is equal to) every function in the set, if such a function
exists.  A special case where ⊗lub is always defined is the following.
Let ⊗⊗f⊗%4i%* be a set of functions satisfying

⊗⊗⊗f%4i%* q≤ f%4i+1%*⊗ for all ⊗i.  

Such a set is called a ⊗chain.  The ⊗lub of a chain  always exists.
Call the resulting function ⊗f,  then we can
compute ⊗f as follows.  If for some ⊗n ⊗⊗f%4n%*[x]_≠_qw⊗ then 
⊗⊗f[x]_=_f%4n%*[x]⊗.  If no such ⊗n exists then ⊗⊗f[x]_=_qw⊗.  This works
because of the simple nature of the partial ordering.
.xgenlines ← xgenlines-2;

	If qt is a functional mapping functons from D1 to D2 to functions of the
same type then a function ⊗f satisfying ⊗⊗f_=_qt[f]⊗ is  a ⊗fixedpoint of qt.
If furthermore for any other function ⊗g we have ⊗⊗g_=_qt[g]_⊃_f_q≤_g⊗  
then ⊗f is the ⊗least ⊗fixedpoint of qt.  For our restricted class of functionals
the least fixedpoint always exists.   We denote the least fixedpoint of qt by
qY[qt].   

	The existence of qY[qt] is due to the fact that our
functionals have some very special properties.  
One such property is ⊗monotonicity.  A functional, qt that 
is monotonic preserves the partial ordering of its function  domain.
In particular, for functions ⊗f and ⊗g, qt must satisfy 

⊗⊗⊗f q≤ g ⊃ qt[f] q≤ qt[g] .		⊗

	A second propery is ⊗continuity.  A continuous functional is monotonic
and must preserve ⊗⊗lub⊗'s of chains of functions.   In particular if qt is
a continuous functional and ⊗⊗f%4i%*⊗ is a chain of functions then
the set ⊗⊗qt[f%4i%*]⊗ of functions is also a chain and

⊗⊗⊗qt[lubα{f%4i%*α}] = lubα{qt[f%4i%*]α}⊗.

	Now we show how to construct qY[qt] for a continuous functional qt.
Let 

⊗⊗⊗f%40%* = qw⊗ and ⊗⊗f%4i+1%* = qt[f%4i%*] ⊗. 

Then 

⊗⊗⊗qw = f%40%* q≤ f%41%* = qt[f%40%*]⊗ 

and, since qt is monotonic, 

⊗⊗⊗f%4i%* q≤ f%4i+1%*⊗ for all ⊗i. 
.xgenlines ← xgenlines-1

Thus the functions ⊗⊗f%4i%*⊗ form a chain,  ⊗⊗lubα{f%4i%*α}⊗ is defined,  
and ⊗⊗qY[qt]_=_lubα{f%4i%*α}⊗ .   
Intuitively one can think of the ⊗⊗f%4i%*⊗'s as forming a sequence of successively
better approximations to the function qY[qt].  What is being approximated is
the domain of definition.  Repeated applications of qt increase the domain of
definition (unless, of course, we have for some ⊗i that ⊗⊗f%4i%*⊗_=_qY[qt]).

	For example if

⊗⊗⊗qt = λf: λx: [qif qat x qthen x qelse f[qa x]] ⊗

then, for ⊗⊗f%41%*⊗ and ⊗⊗f%42%*⊗ as defined above, we have

⊗⊗⊗f%41%* = qt[qw]⊗ and ⊗⊗f%42%* = qt[f%41%*] ⊗.   

The ⊗n mentioned above in the description of how to compute ⊗lub of a chain 
of functions is
essentially the number of ⊗⊗car⊗'s that must be applied to ⊗x to reach an atom.


[A parenthetical remark:  the notions of ⊗monotonicity and ⊗continuity defined
above are generalizations of those encountered in a calculus or analysis course
in mathematics.  Such generalizations are common in the study of topology
and the above arguments can be formulated in a topological framework.]
.xgenlines←xgenlines-3;


	Now we are ready to define the function computed by a recursive program
and to show how this function is characterized by the corresponding functional
equation in the case of total functions.  If qt is a term_functional then 
the function, ⊗f, computed by the recursive program,
⊗⊗f_x_←_qt[f]_x⊗  is qY[qt].  
Thus ⊗f satisfies the functional equation

⊗⊗⊗∀x: [f x = qt[f] x] .		⊗

If ⊗f is total then ⊗⊗f_x_≠_qw⊗ for any ⊗x in D1.  This means that for any function
⊗g 

⊗⊗⊗f q≤ g⊗  iff ⊗⊗f = g .		⊗

Thus ⊗f is the unique function satisfying the functional equation.

	In the case that ⊗f is
not total the functional equation is not sufficient. We also need to express the
fact that ⊗f is the least function satisfying this equation.   The minimization
schema will do that.

.ss The Minimization Schema.

	As mentioned before, the functional equation of a program doesn't 
in general completely characterize it.  For example, the program

⊗⊗⊗f1 x ← f1 x			⊗

leads to the sentence

⊗⊗⊗∀x: [f1 x = f1 x]		⊗

which provides no information although the function ⊗f1 
is undefined for all ⊗x.  This is not always the case, since
the program

⊗⊗⊗f2 x ← [f2 x] . qNIL		⊗

has the functional equation

⊗⊗⊗∀x: [f2 x = [f2 x] . qNIL] .	⊗

from which ⊗⊗∀x: [¬issexp f2 x]⊗ can be proved by induction.

	In order to characterize recursive programs, we need some
way of asking for the least defined solution of the functional equation.  That is 
we want the least fixedpoint of the defining functional. 

	Consider the recursive program 

⊗⊗⊗f x ← qt[f] x 		⊗

which has the functional equation

⊗⊗⊗∀x: [f x = qt[f] x] .	⊗

It can be shown that requiring a fixedpoint ⊗f of a functional qt to be minimal
is equivalent to the ⊗minimization_schema  

⊗⊗⊗∀x: [qt[F] x q≤ F x] ⊃ ∀x: [f x q≤ F x]⊗

where ⊗F is a function variable.

	The partial ordering can be removed from the statement of the 
minimization schema by noting that for functions ⊗f and ⊗g we have

⊗⊗⊗f q≤ g ≡ ∀x: [isD f x ⊃ f x = g x]⊗

where D is the domain containing the range of ⊗f and the predicate ⊗isD states that
its argument is in the domain D. Thus ⊗⊗isD_f_x⊗ means that ⊗⊗f_x_≠_qw⊗.
The minimization schema then becomes

⊗⊗⊗∀x: [isD qt[F] x ⊃ F x = qt[F] x] ⊃ ∀x: [isD f x ⊃ f x = F x] ⊗.


	The simplest application of the schema is to show that the program for 
⊗f1 given above computes the totally undefined function.
The schema becomes

⊗⊗⊗∀x: [F x q≤ F x] ⊃ ∀x: [f1 x q≤ F x] ⊗.

The left side of the implication is identically true.  
Taking F[x] = qw,  and remembering that
⊗⊗X_q≤_qw⊗ only if ⊗⊗X_=_qw⊗, the right side tells us that ⊗⊗f1_x_=_qw⊗.

	The minimization schema provides an alternate method for proving the 
correctness of ⊗samefringe.  To simplify matters we eliminate the auxilliary
function ⊗samea from the definition of ⊗samefringea thus eliminating the problem
of having to deal with mutually recursive programs.  The functional defining
⊗samefringea now becomes
.NOFILL

⊗⊗⊗qt = λF: λx y: [[x eeq y] oor [[nnot aatom x aand nnot aatom y] aand 			⊗
⊗⊗⊗		[[qa gopher x eeq qa gopher y] aand F[qd gopher x, qd gopher y]]]] ⊗.
.FILL

Now we form an axiom schema from the minimization schema by using the qt
given above and ⊗samefringea for ⊗f. 
We instantiate this schema with 

⊗⊗⊗F[x, y] = fringe x eeq fringe y  .		⊗

The proof then consists of the following steps

	1) 	⊗⊗∀x y: [istv qt[F] [x, y]]⊗

	2)	⊗⊗∀x y: [F[x, y] = qt[F] [x, y]]⊗

	3)	⊗⊗∀x y: istv samefringea[x, y]⊗

from 1) - 3) and the axiom instantiation we conclude

	4)	⊗⊗∀x y: [fringe x eeq fringe y = samefringea[x, y]]⊗

from 3) we know that ⊗samefringea[x,_y] is either $TT or $FF and so by a simple
case analysis using the TV-lemmas, the fact that $TT ≠ $FF,
the definition of ⊗samefringe and 4) we conclude

	5)	⊗⊗∀x y: [samefringe[x, y] ≡ fringe x = fringe y]⊗

as desired.


	The minimization schema can sometimes be used to show partial
correctness.  For example, the well known 91-function is defined by
the recursive program over the integers

⊗⊗⊗f91 x ← qif x > 100 qthen x - 10 qelse f91 f91 [x + 11] ⊗.

The goal is to show that

⊗⊗⊗∀x: [f91 x = qif x > 100 qthen x - 10 qelse 91] .	⊗

We apply the minimization schema with

⊗⊗⊗F x = qif x > 100 qthen x - 10 qelse 91 ,		⊗

and it can be shown by an explicit calculation without induction that
the premiss of the schema is satisfied, and this shows that ⊗f91, 
whenever defined has the desired value.

	The method of ⊗recursion ⊗induction is also
an immediate application of the minimization schema.  If we show
that two functions satisfy the schema of a recursive program, we
show that they both equal the function computed by the program 
whereever the function is defined.

	The utility of the minimization schema for proving partial
correctness or non-termination depends on our ability to name
suitable comparison functions.  ⊗f1 and ⊗f91 were easily treated,
because the necessary comparison functions could be given explicitly
without recursion.  Any extension of the language that provides new
tools for naming comparison functions, e.g. going to higher order
logic, will improve our ability to use the schema in proofs.

	The minimization schema can be regarded as an axiom schema involving
a second order function variable qt.  What can be substituted
for qt is a  quantifier free
λ-expression in a first order function variable.
It may be interesting to study the sets of first order sentences that
can be generated by such second order sentence schemata.  Presumably,
sets of sentences can be generated in this way that cannnot be
generated by schemata with only first order function variables.
.cb Exercises.
.item←0
#. Simple structural induction proofs.
Prove the following statements.

	##.	⊗⊗∀u: u * qNIL = u⊗

	##. 	⊗⊗∀u: islist reverse1 u⊗

	##. 	⊗⊗∀u: reverse u = reverse1 u⊗

	##.	⊗⊗∀u v: reverse[u * v] = [reverse v] * [reverse u]⊗

	##.  	⊗⊗∀u: reverse reverse u = u⊗

	##. 	⊗⊗∀x: flatten x = fringe x⊗

	##. 	⊗⊗∀x: (¬qat x ⊃ size gopher x = size x)⊗

	##.  	⊗⊗∀x: (¬qat x ⊃ qat qa gopher x)⊗

where the necessary LISP function definitions are:

		⊗⊗u * v ← qif qn u qthen v qelse qa u . [qd u * v]⊗

		⊗⊗reverse1 u ← if qn u qthen qNIL qelse [reverse1 qd u] * <qa u>⊗

		⊗⊗reverse u ← rev[u, qNIL]⊗

		⊗⊗rev[u, v] ← qif qn u qthen v qelse rev[qd u, qa u . v]⊗

		⊗⊗flatten x ← flat[x, qNIL]⊗

		⊗⊗flat[x, u] ← qif qat x qthen [x . u] qelse flat[qa x, flat[qd x, u]]⊗

		⊗⊗fringe x ← qif qat x qthen <x> qelse [fringe qa x] * [fringe qd x]⊗

		⊗⊗gopher x ← qif qat qa x qthen x qelse gopher[qaa x . [qda x . qd x]]⊗

		⊗⊗size x ← qif qat x qthen 1 qelse size qa x + size qd x⊗



.bb 2. Properties of substitutions and substitution lists.

	With function definitions as given below,
⊗⊗subst[x,_y,_z]⊗ is the result of replacing the variable ⊗y by the
S-expression ⊗x whereever ⊗y occurs in ⊗z.  If ⊗s is a list of substitutions of 
the form ⊗⊗y_._x⊗ then ⊗⊗sublis[z,_s]⊗ is the result of "simultaneously" performing
all of the substitutions on the list to ⊗z. If ⊗s1 and ⊗s2 are lists of substitutions
then ⊗s1 @ ⊗s2 is "composition"  of the two.  Prove the following properties.

.NOFILL

	i)	⊗⊗∀x y z: subst[x, y, z] = sublis[z, <y . x>]⊗

	ii)	⊗⊗∀z s1 s2: sublis[z, s1 @ s2] = sublis[sublis[z, s1], s2]⊗

	iii)	⊗⊗∀z s1 s2 s3: sublis[z, s1 @ [s2 @ s3]] = sublis[z, [s1 @ s2] @ s3]⊗

	iv)	⊗⊗∀x y z: (¬occur[y, z] ⊃ subst[x, y, z] = z)⊗

	v) 	⊗⊗∀x x1 y y1 z: ((y ≠  y1 ∧ ¬occur[y, x1]) ⊃ ⊗
	    		⊗⊗subst[x1, y1, subst[x, y, z]] = subst[subst[x1, y1, x], y, subst[x1, y1, z]])⊗


where

	⊗⊗assoc[x, s] ← qif qn s qthen qNIL qelse qif x = qaa s qthen qa s qelse assoc[x, qd s]⊗

	⊗⊗subst[x, y, z] ← qif qat z qthen [qif y = z qthen x qelse z] ⊗
			⊗⊗qelse subst[x, y, qa z] . subst[x, y, qd z]⊗

	⊗⊗occur[x, y] ← [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]⊗.

	⊗⊗sublis[x, s] ← qif qat x qthen α{assoc[x, s]α}[λz: qif qn z qthen x qelse qd z]⊗
			⊗⊗qelse sublis[qa x, s] . sublis[qd x, s]⊗

	⊗⊗s1 @ s2 ← subsub[s1, s2] * s2⊗

	⊗⊗subsub[s1, s2] ← qif qn s1 qthen qNIL qelse [qaa s1 . sublis[qda s1, s2]] . subsub[qd s1, s2]⊗
.FILL

.bb 3. Pattern matching and unification properties.

	(This is a fairly substantial exercise.)  


	With the further function definitions given below, ⊗⊗inst[x,_y,_qNIL]⊗ is
$NO if ⊗x is not and instance of the pattern ⊗y, and otherwise is the list of
substitions which will convert ⊗y into ⊗x.  In the latter case we have
⊗⊗x_=_sublis[y,_inst[x,_y,_qNIL]⊗.  Prove

	i)	⊗⊗∀x y s: (inst[x, y, s] ≠ $NO ⊃ x = sublis[y, inst[x, y, s]])⊗

	⊗unify[x,y] attempts to find the most general 
pattern which is an instance of both ⊗x and ⊗y. If no such pattern exists the it
returns $NO, otherwise it returns a list of substitutions which will convert both
⊗x and ⊗y into that pattern.  Prove

	ii)	⊗⊗∀x y: (unify[x, y] ≠ $NO ⊃ sublis[x, unify[x, y]] = sublis[y, unify[x, y]])⊗

	iii)	⊗⊗∀x y: (unify[x, y] = $NO ⊃ ∀s: sublis[x, s] ≠ sublis[y, s])⊗

	iv)	⊗⊗∀x y s: (sublis[x, s] = sublis[y, s] ⊃ ∃s1: ∀z: sublis[z, s] = sublis[z, unify[x, y] @ s1])⊗

where


.NOFILL

	⊗⊗inst[x, y, s] ← qif s = $NO qthen $NO ⊗
		⊗⊗qelse qif qat y qthen [qif isvar y qthen ⊗
				⊗⊗α{assoc[y, s]α}[λz: qif qn z qthen [y . x] . s qelse qif qd z = x qthen s qelse $NO ]⊗
			⊗⊗qelse qif y = x qthen s qelse $NO ]⊗
	    	⊗⊗qelse qif qat x qthen $NO ⊗
		⊗⊗qelse inst[qd x, qd y, inst[qa x, qa y, s]]⊗

	⊗⊗isvar x ← x = $U ∨ x = $V ∨ x = $W ∨ x = $X ∨ x = $Y ∨ x = $Z ⊗

	⊗⊗unify[x, y] ← qif x = y qthen qNIL⊗
		⊗⊗qelse qif isvar x qthen [qif occur[x, y] qthen $NO qelse <x . y>]⊗
		⊗⊗qelse qif isvar y qthen [qif occur[y, x] qthen $NO qelse <y . x>]⊗
		⊗⊗qelse qif [qat x ∨ qat y] qthen $NO ⊗
		⊗⊗qelse α{unify[qa x,qa y]α}⊗
			⊗⊗[λs1: qif s1 = $NO qthen $NO ⊗
			    ⊗⊗qelse α{unify[sublis[qd x, s1],sublis[qd y, s1]]α}⊗
				⊗⊗[λs2: qif s2 = $NO qthen $NO qelse s1 @ s2]]⊗

.FILL